Bei sehr vielen Einträgen in die MakeTeXFont.sh-Datei wird
MakeBatch sehr langsam, das heißt es braucht circa eine Minute
pro Eintrag. Da dann allerdings auch schon über 100 Aufrufe von
MakeTeXFont.rexx eingetragen sind und diese im Durchschnitt über
30 Minuten dauern, dürfte der Zeitverlust zu verkraften sein.